Lemma everything_implies_itself:
  forall p:Prop, p -> p.
Proof.
  intros.
  assumption.
Qed.